A primary aim of a reliable software system is ensuring that all objects in the system maintain consistent states; that is, states in which all fields of an object, and all fields of other objects upon which it depends, contain legal, meaningful values. If an object contains only legal values, it is considered to maintain invariancy. It is difficult to maintain invariants in sequential programs, as an object invariant may temporarily be violated during the update of an object's data, and any method call performed during this time may potentially cause control to re-enter the object's public interface where the object invariant is expected to hold.
It is even harder in concurrent object-oriented programs. For example, consider a system where for all dual accounts, account a and account b are to sum to the value zero. Consider the code fragment shown below:
void Transfer(DualAccounts o, int amount) {  o.a := o.a − amount;  o.b := o.b + amount;}
In a sequential setting, this code maintains the invariant. However, in a system where more than one thread is running concurrently, the invariant condition (a+b=0) can be violated. It is not possible for a program to change the values in o.a and o.b simultaneously, which allows for the possibility of invariant violation, and can also lead to inconsistent program behavior. Such inconsistencies are known as dataraces. A datarace occurs in an execution of a program where there are conflicting actions in multiple threads when the actions are not explicitly ordered.
One method to ensure invariancy is to guarantee that an individual update is atomic. That is, each update will be performed with no other code updates on other threads occurring until the operation is complete. This ensures that the value of o.a, for example, will not be changed while the line of code o.a:=o.a−amount is being processed. This is insufficient to prevent the invariancy from being violated, as an update to a or b could occur on a different thread between the subtraction and the addition steps.
For example, FIG. 1A shows a program that starts two instances (t1 and t2) of code designed to increment a global counter S_count by 1. FIG. 1B shows the code executed (on two threads) the way the programmer expected; statements 1, 2, 3, and 4 are executed in order, with the result that the counter S_count is incremented as envisioned. In FIG. 1C, the second instantiation of IncrCount is interleaved between the two lines of code in the first instantiation with the effect that the value of x in t1 is not changed after its value is stored at line “1” of code in FIG. 1, when it is read by t2. So, the counter S_count is incremented only once after both t1 and t2 have run; leaving the value of S_count at “1”, rather than the expected “2”.
One method used to ensure internal consistency in a multi-threaded environment is by enforcing atomicity of concurrent operations at a level coarser than individual reads and writes. Commonly, the objects being updated are locked using mutexes. The following procedure will ensure that, for the Transfer function below, invariancy would be maintained:
void Transfer(DualAccounts o, int amount) {    Lock Mutex for o.a    Lock Mutex for o.b    o.a:=o.a − amount;    o.b:=o.b + amount;    Unlock Mutex for o.a    Unlock Mutex for o.b  }However, mutex locks are expensive in terms of CPU time, and can cause other problems—such as starvation conditions, deadlocks, and race conditions; all of which can be very difficult to locate and debug, dependent as they are on very specific thread-statement ordering, such as that shown in FIG. 1C.
Extended Static Checkers for Modula-3 and for Java attempt to statically find errors in object-oriented programs. These tools include support for the prevention of dataraces and deadlocks. For each field, a programmer can designate which lock protects it. However, these two tools trade soundness for ease of use; for example, they do not take into consideration the effects of other threads between regions of exclusion. Moreover, various engineering trade-offs in the tools notwithstanding, the methodology used by the tools was never formalized enough to allow a soundness proof.